(set-logic QF_UFLRA)
(set-info :source |CPAchecker with k-induction on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)


(declare-fun |IofCallDriver::__cil_tmp8@3| () Real)
(declare-fun |IofCallDriver::Irp__PendingReturned@3| () Real)
(declare-fun routine@4 () Real)
(declare-fun UNLOADED@4 () Real)
(declare-fun |__ADDRESS_OF_CdAudioDeviceControl::status| () Real)
(declare-fun __ADDRESS_OF_DC () Real)
(declare-fun |__ADDRESS_OF_IofCallDriver::compRetStatus| () Real)
(declare-fun |__ADDRESS_OF_IofCallDriver::returnVal2| () Real)
(declare-fun __ADDRESS_OF_IPC () Real)
(declare-fun |HPCdrCompletion::Irp__PendingReturned@3| () Real)
(declare-fun __ADDRESS_OF_SKIP1 () Real)
(declare-fun __ADDRESS_OF_compFptr () Real)
(declare-fun setEventCalled@6 () Real)
(declare-fun |__ADDRESS_OF_CdAudioHPCdrDeviceControl::__cil_tmp12| () Real)
(declare-fun |main::tmp_ndt_1@3| () Real)
(declare-fun compFptr@5 () Real)
(declare-fun __ADDRESS_OF_DeviceUsageTypePaging () Real)
(declare-fun setEventCalled@2 () Real)
(declare-fun setEventCalled@3 () Real)
(declare-fun __ADDRESS_OF_MPR3 () Real)
(declare-fun MPR3@4 () Real)
(declare-fun lowerDriverReturn@6 () Real)
(declare-fun myStatus@3 () Real)
(declare-fun |IofCallDriver::__retval__@2| () Real)
(declare-fun IPC@4 () Real)
(declare-fun s@7 () Real)
(declare-fun NP@3 () Real)
(declare-fun |main::status@4| () Real)
(declare-fun MPR1@3 () Real)
(declare-fun MPR3@2 () Real)
(declare-fun |CdAudioDeviceControl::status@3| () Real)
(declare-fun pended@7 () Real)
(declare-fun |__ADDRESS_OF_CdAudioDeviceControl::deviceExtension__Active| () Real)
(declare-fun __ADDRESS_OF_NP () Real)
(declare-fun pended@2 () Real)
(declare-fun pended@5 () Real)
(declare-fun NP@4 () Real)
(declare-fun customIrp@4 () Real)
(declare-fun MPR1@2 () Real)
(declare-fun lowerDriverReturn@4 () Real)
(declare-fun __ADDRESS_OF_MPR1 () Real)
(declare-fun SKIP1@4 () Real)
(declare-fun __ADDRESS_OF_compRegistered () Real)
(declare-fun |__ADDRESS_OF_main::we_should_unload| () Real)
(declare-fun MPR1@4 () Real)
(declare-fun |IofCallDriver::returnVal2@3| () Real)
(declare-fun |CdAudioHPCdrDeviceControl::__cil_tmp12@3| () Real)
(declare-fun compFptr@6 () Real)
(declare-fun compRegistered@3 () Real)
(declare-fun DeviceUsageTypePaging@3 () Real)
(declare-fun |CdAudioDeviceControl::deviceExtension__Active@3| () Real)
(declare-fun DC@2 () Real)
(declare-fun |CdAudioHPCdrDeviceControl::__retval__@2| () Real)
(declare-fun DeviceUsageTypePaging@2 () Real)
(declare-fun compRegistered@6 () Real)
(declare-fun s@4 () Real)
(declare-fun myStatus@4 () Real)
(declare-fun __ADDRESS_OF_setEventCalled () Real)
(declare-fun DC@3 () Real)
(declare-fun __ADDRESS_OF_routine () Real)
(declare-fun __ADDRESS_OF_UNLOADED () Real)
(declare-fun setEventCalled@4 () Real)
(declare-fun SKIP2@2 () Real)
(declare-fun MPR3@3 () Real)
(declare-fun customIrp@5 () Real)
(declare-fun |CdAudioDeviceControl::__retval__@2| () Real)
(declare-fun s@6 () Real)
(declare-fun |CdAudioHPCdrDeviceControl::tmp@3| () Real)
(declare-fun __ADDRESS_OF_SKIP2 () Real)
(declare-fun myStatus@2 () Real)
(declare-fun __ADDRESS_OF_pended () Real)
(declare-fun lowerDriverReturn@2 () Real)
(declare-fun pended@4 () Real)
(declare-fun compRegistered@2 () Real)
(declare-fun |__ADDRESS_OF_main::irp_choice| () Real)
(declare-fun pended@6 () Real)
(declare-fun |IofCallDriver::tmp_ndt_4@3| () Real)
(declare-fun |CdAudioHPCdrDeviceControl::currentIrpStack__Parameters__DeviceIoControl__IoControlCode@3| () Real)
(declare-fun |__ADDRESS_OF_IofCallDriver::tmp_ndt_4| () Real)
(declare-fun customIrp@3 () Real)
(declare-fun UNLOADED@2 () Real)
(declare-fun lowerDriverReturn@5 () Real)
(declare-fun s@2 () Real)
(declare-fun |__ADDRESS_OF_main::status| () Real)
(declare-fun __ADDRESS_OF_customIrp () Real)
(declare-fun SKIP1@3 () Real)
(declare-fun customIrp@6 () Real)
(declare-fun customIrp@2 () Real)
(declare-fun |IofCallDriver::compRetStatus@3| () Real)
(declare-fun IPC@3 () Real)
(declare-fun |__ADDRESS_OF_IofCallDriver::__cil_tmp8| () Real)
(declare-fun compRegistered@7 () Real)
(declare-fun IPC@2 () Real)
(declare-fun compFptr@3 () Real)
(declare-fun compFptr@4 () Real)
(declare-fun |__ADDRESS_OF_CdAudioHPCdrDeviceControl::tmp___0| () Real)
(declare-fun s@3 () Real)
(declare-fun |__ADDRESS_OF_HPCdrCompletion::Irp__PendingReturned| () Real)
(declare-fun __ADDRESS_OF_myStatus () Real)
(declare-fun DC@4 () Real)
(declare-fun |HPCdrCompletion::__retval__@2| () Real)
(declare-fun myStatus@5 () Real)
(declare-fun compRegistered@5 () Real)
(declare-fun SKIP2@4 () Real)
(declare-fun s@5 () Real)
(declare-fun setEventCalled@5 () Real)
(declare-fun __ADDRESS_OF_s () Real)
(declare-fun __ADDRESS_OF_lowerDriverReturn () Real)
(declare-fun lowerDriverReturn@3 () Real)
(declare-fun |main::status@3| () Real)
(declare-fun NP@2 () Real)
(declare-fun lowerDriverReturn@7 () Real)
(declare-fun |__ADDRESS_OF_IofCallDriver::Irp__PendingReturned| () Real)
(declare-fun routine@3 () Real)
(declare-fun |__ADDRESS_OF_CdAudioHPCdrDeviceControl::currentIrpStack__Parameters__DeviceIoControl__IoControlCode| () Real)
(declare-fun UNLOADED@3 () Real)
(declare-fun |__ADDRESS_OF_CdAudioHPCdrDeviceControl::tmp| () Real)
(declare-fun |__ADDRESS_OF_main::tmp_ndt_1| () Real)
(declare-fun SKIP1@2 () Real)
(declare-fun routine@2 () Real)
(declare-fun SKIP2@3 () Real)
(declare-fun compRegistered@4 () Real)
(declare-fun |main::irp_choice@3| () Real)
(declare-fun pended@3 () Real)
(declare-fun |main::we_should_unload@3| () Real)
(declare-fun compFptr@2 () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real __ADDRESS_OF_s)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real s@2)
(define-fun _12 () Bool (= _11 _7))
(define-fun _13 () Bool (and _10 _12))
(define-fun _14 () Real __ADDRESS_OF_UNLOADED)
(define-fun _15 () Real (__BASE_ADDRESS_OF__ _14))
(define-fun _16 () Bool (= _14 _15))
(define-fun _17 () Real UNLOADED@2)
(define-fun _18 () Bool (= _17 _7))
(define-fun _19 () Bool (and _16 _18))
(define-fun _20 () Bool (and _13 _19))
(define-fun _21 () Real __ADDRESS_OF_NP)
(define-fun _22 () Real (__BASE_ADDRESS_OF__ _21))
(define-fun _23 () Bool (= _21 _22))
(define-fun _24 () Real NP@2)
(define-fun _25 () Bool (= _24 _7))
(define-fun _26 () Bool (and _23 _25))
(define-fun _27 () Bool (and _20 _26))
(define-fun _28 () Real __ADDRESS_OF_DC)
(define-fun _29 () Real (__BASE_ADDRESS_OF__ _28))
(define-fun _30 () Bool (= _28 _29))
(define-fun _31 () Real DC@2)
(define-fun _32 () Bool (= _31 _7))
(define-fun _33 () Bool (and _30 _32))
(define-fun _34 () Bool (and _27 _33))
(define-fun _35 () Real __ADDRESS_OF_SKIP1)
(define-fun _36 () Real (__BASE_ADDRESS_OF__ _35))
(define-fun _37 () Bool (= _35 _36))
(define-fun _38 () Real SKIP1@2)
(define-fun _39 () Bool (= _38 _7))
(define-fun _40 () Bool (and _37 _39))
(define-fun _41 () Bool (and _34 _40))
(define-fun _42 () Real __ADDRESS_OF_SKIP2)
(define-fun _43 () Real (__BASE_ADDRESS_OF__ _42))
(define-fun _44 () Bool (= _42 _43))
(define-fun _45 () Real SKIP2@2)
(define-fun _46 () Bool (= _45 _7))
(define-fun _47 () Bool (and _44 _46))
(define-fun _48 () Bool (and _41 _47))
(define-fun _49 () Real __ADDRESS_OF_MPR1)
(define-fun _50 () Real (__BASE_ADDRESS_OF__ _49))
(define-fun _51 () Bool (= _49 _50))
(define-fun _52 () Real MPR1@2)
(define-fun _53 () Bool (= _52 _7))
(define-fun _54 () Bool (and _51 _53))
(define-fun _55 () Bool (and _48 _54))
(define-fun _56 () Real __ADDRESS_OF_MPR3)
(define-fun _57 () Real (__BASE_ADDRESS_OF__ _56))
(define-fun _58 () Bool (= _56 _57))
(define-fun _59 () Real MPR3@2)
(define-fun _60 () Bool (= _59 _7))
(define-fun _61 () Bool (and _58 _60))
(define-fun _62 () Bool (and _55 _61))
(define-fun _63 () Real __ADDRESS_OF_IPC)
(define-fun _64 () Real (__BASE_ADDRESS_OF__ _63))
(define-fun _65 () Bool (= _63 _64))
(define-fun _66 () Real IPC@2)
(define-fun _67 () Bool (= _66 _7))
(define-fun _68 () Bool (and _65 _67))
(define-fun _69 () Bool (and _62 _68))
(define-fun _70 () Real __ADDRESS_OF_pended)
(define-fun _71 () Real (__BASE_ADDRESS_OF__ _70))
(define-fun _72 () Bool (= _70 _71))
(define-fun _73 () Real pended@2)
(define-fun _74 () Bool (= _73 _7))
(define-fun _75 () Bool (and _72 _74))
(define-fun _76 () Bool (and _69 _75))
(define-fun _77 () Real __ADDRESS_OF_compFptr)
(define-fun _78 () Real (__BASE_ADDRESS_OF__ _77))
(define-fun _79 () Bool (= _77 _78))
(define-fun _80 () Real compFptr@2)
(define-fun _81 () Bool (= _80 _7))
(define-fun _82 () Bool (and _79 _81))
(define-fun _83 () Bool (and _76 _82))
(define-fun _84 () Real __ADDRESS_OF_compRegistered)
(define-fun _85 () Real (__BASE_ADDRESS_OF__ _84))
(define-fun _86 () Bool (= _84 _85))
(define-fun _87 () Real compRegistered@2)
(define-fun _88 () Bool (= _87 _7))
(define-fun _89 () Bool (and _86 _88))
(define-fun _90 () Bool (and _83 _89))
(define-fun _91 () Real __ADDRESS_OF_lowerDriverReturn)
(define-fun _92 () Real (__BASE_ADDRESS_OF__ _91))
(define-fun _93 () Bool (= _91 _92))
(define-fun _94 () Real lowerDriverReturn@2)
(define-fun _95 () Bool (= _94 _7))
(define-fun _96 () Bool (and _93 _95))
(define-fun _97 () Bool (and _90 _96))
(define-fun _98 () Real __ADDRESS_OF_setEventCalled)
(define-fun _99 () Real (__BASE_ADDRESS_OF__ _98))
(define-fun _100 () Bool (= _98 _99))
(define-fun _101 () Real setEventCalled@2)
(define-fun _102 () Bool (= _101 _7))
(define-fun _103 () Bool (and _100 _102))
(define-fun _104 () Bool (and _97 _103))
(define-fun _105 () Real __ADDRESS_OF_customIrp)
(define-fun _106 () Real (__BASE_ADDRESS_OF__ _105))
(define-fun _107 () Bool (= _105 _106))
(define-fun _108 () Real customIrp@2)
(define-fun _109 () Bool (= _108 _7))
(define-fun _110 () Bool (and _107 _109))
(define-fun _111 () Bool (and _104 _110))
(define-fun _112 () Real __ADDRESS_OF_routine)
(define-fun _113 () Real (__BASE_ADDRESS_OF__ _112))
(define-fun _114 () Bool (= _112 _113))
(define-fun _115 () Real routine@2)
(define-fun _116 () Bool (= _115 _7))
(define-fun _117 () Bool (and _114 _116))
(define-fun _118 () Bool (and _111 _117))
(define-fun _119 () Real __ADDRESS_OF_myStatus)
(define-fun _120 () Real (__BASE_ADDRESS_OF__ _119))
(define-fun _121 () Bool (= _119 _120))
(define-fun _122 () Real myStatus@2)
(define-fun _123 () Bool (= _122 _7))
(define-fun _124 () Bool (and _121 _123))
(define-fun _125 () Bool (and _118 _124))
(define-fun _126 () Real __ADDRESS_OF_DeviceUsageTypePaging)
(define-fun _127 () Real (__BASE_ADDRESS_OF__ _126))
(define-fun _128 () Bool (= _126 _127))
(define-fun _129 () Real DeviceUsageTypePaging@2)
(define-fun _130 () Bool (= _129 _7))
(define-fun _131 () Bool (and _128 _130))
(define-fun _132 () Bool (and _125 _131))
(define-fun _133 () Real |__ADDRESS_OF_main::status|)
(define-fun _134 () Real (__BASE_ADDRESS_OF__ _133))
(define-fun _135 () Bool (= _133 _134))
(define-fun _136 () Bool (and _132 _135))
(define-fun _137 () Real |__ADDRESS_OF_main::we_should_unload|)
(define-fun _138 () Real (__BASE_ADDRESS_OF__ _137))
(define-fun _139 () Bool (= _137 _138))
(define-fun _140 () Bool (and _136 _139))
(define-fun _141 () Real |__ADDRESS_OF_main::irp_choice|)
(define-fun _142 () Real (__BASE_ADDRESS_OF__ _141))
(define-fun _143 () Bool (= _141 _142))
(define-fun _144 () Bool (and _140 _143))
(define-fun _145 () Real s@3)
(define-fun _146 () Bool (= _145 _7))
(define-fun _147 () Bool (and _144 _146))
(define-fun _148 () Real UNLOADED@3)
(define-fun _149 () Bool (= _148 _7))
(define-fun _150 () Bool (and _147 _149))
(define-fun _151 () Real NP@3)
(define-fun _152 () Bool (= _151 _7))
(define-fun _153 () Bool (and _150 _152))
(define-fun _154 () Real DC@3)
(define-fun _155 () Bool (= _154 _7))
(define-fun _156 () Bool (and _153 _155))
(define-fun _157 () Real SKIP1@3)
(define-fun _158 () Bool (= _157 _7))
(define-fun _159 () Bool (and _156 _158))
(define-fun _160 () Real SKIP2@3)
(define-fun _161 () Bool (= _160 _7))
(define-fun _162 () Bool (and _159 _161))
(define-fun _163 () Real MPR1@3)
(define-fun _164 () Bool (= _163 _7))
(define-fun _165 () Bool (and _162 _164))
(define-fun _166 () Real MPR3@3)
(define-fun _167 () Bool (= _166 _7))
(define-fun _168 () Bool (and _165 _167))
(define-fun _169 () Real IPC@3)
(define-fun _170 () Bool (= _169 _7))
(define-fun _171 () Bool (and _168 _170))
(define-fun _172 () Real pended@3)
(define-fun _173 () Bool (= _172 _7))
(define-fun _174 () Bool (and _171 _173))
(define-fun _175 () Real compFptr@3)
(define-fun _176 () Bool (= _175 _7))
(define-fun _177 () Bool (and _174 _176))
(define-fun _178 () Real compRegistered@3)
(define-fun _179 () Bool (= _178 _7))
(define-fun _180 () Bool (and _177 _179))
(define-fun _181 () Real lowerDriverReturn@3)
(define-fun _182 () Bool (= _181 _7))
(define-fun _183 () Bool (and _180 _182))
(define-fun _184 () Real setEventCalled@3)
(define-fun _185 () Bool (= _184 _7))
(define-fun _186 () Bool (and _183 _185))
(define-fun _187 () Real customIrp@3)
(define-fun _188 () Bool (= _187 _7))
(define-fun _189 () Bool (and _186 _188))
(define-fun _190 () Real routine@3)
(define-fun _191 () Bool (= _190 _7))
(define-fun _192 () Bool (and _189 _191))
(define-fun _193 () Real myStatus@3)
(define-fun _194 () Bool (= _193 _7))
(define-fun _195 () Bool (and _192 _194))
(define-fun _196 () Real 1)
(define-fun _197 () Real DeviceUsageTypePaging@3)
(define-fun _198 () Bool (= _197 _196))
(define-fun _199 () Bool (and _195 _198))
(define-fun _200 () Real UNLOADED@4)
(define-fun _201 () Bool (= _200 _7))
(define-fun _202 () Bool (and _199 _201))
(define-fun _203 () Real NP@4)
(define-fun _204 () Bool (= _203 _196))
(define-fun _205 () Bool (and _202 _204))
(define-fun _206 () Real 2)
(define-fun _207 () Real DC@4)
(define-fun _208 () Bool (= _207 _206))
(define-fun _209 () Bool (and _205 _208))
(define-fun _210 () Real 3)
(define-fun _211 () Real SKIP1@4)
(define-fun _212 () Bool (= _211 _210))
(define-fun _213 () Bool (and _209 _212))
(define-fun _214 () Real 4)
(define-fun _215 () Real SKIP2@4)
(define-fun _216 () Bool (= _215 _214))
(define-fun _217 () Bool (and _213 _216))
(define-fun _218 () Real 5)
(define-fun _219 () Real MPR1@4)
(define-fun _220 () Bool (= _219 _218))
(define-fun _221 () Bool (and _217 _220))
(define-fun _222 () Real 6)
(define-fun _223 () Real MPR3@4)
(define-fun _224 () Bool (= _223 _222))
(define-fun _225 () Bool (and _221 _224))
(define-fun _226 () Real 7)
(define-fun _227 () Real IPC@4)
(define-fun _228 () Bool (= _227 _226))
(define-fun _229 () Bool (and _225 _228))
(define-fun _230 () Real s@4)
(define-fun _231 () Bool (= _200 _230))
(define-fun _232 () Bool (and _229 _231))
(define-fun _233 () Real pended@4)
(define-fun _234 () Bool (= _233 _7))
(define-fun _235 () Bool (and _232 _234))
(define-fun _236 () Real compFptr@4)
(define-fun _237 () Bool (= _236 _7))
(define-fun _238 () Bool (and _235 _237))
(define-fun _239 () Real compRegistered@4)
(define-fun _240 () Bool (= _239 _7))
(define-fun _241 () Bool (and _238 _240))
(define-fun _242 () Real lowerDriverReturn@4)
(define-fun _243 () Bool (= _242 _7))
(define-fun _244 () Bool (and _241 _243))
(define-fun _245 () Real setEventCalled@4)
(define-fun _246 () Bool (= _245 _7))
(define-fun _247 () Bool (and _244 _246))
(define-fun _248 () Real customIrp@4)
(define-fun _249 () Bool (= _248 _7))
(define-fun _250 () Bool (and _247 _249))
(define-fun _251 () Real |main::status@3|)
(define-fun _252 () Bool (<= _7 _251))
(define-fun _254 () Bool (and _250 _252))
(define-fun _257 () Real s@5)
(define-fun _258 () Bool (= _203 _257))
(define-fun _259 () Bool (and _254 _258))
(define-fun _260 () Real customIrp@5)
(define-fun _261 () Bool (= _260 _7))
(define-fun _262 () Bool (and _259 _261))
(define-fun _263 () Real setEventCalled@5)
(define-fun _264 () Bool (= _260 _263))
(define-fun _265 () Bool (and _262 _264))
(define-fun _266 () Real lowerDriverReturn@5)
(define-fun _267 () Bool (= _263 _266))
(define-fun _268 () Bool (and _265 _267))
(define-fun _269 () Real compRegistered@5)
(define-fun _270 () Bool (= _266 _269))
(define-fun _271 () Bool (and _268 _270))
(define-fun _272 () Real compFptr@5)
(define-fun _273 () Bool (= _269 _272))
(define-fun _274 () Bool (and _271 _273))
(define-fun _275 () Real pended@5)
(define-fun _276 () Bool (= _272 _275))
(define-fun _277 () Bool (and _274 _276))
(define-fun _278 () Real myStatus@4)
(define-fun _279 () Bool (= _278 _7))
(define-fun _280 () Bool (and _277 _279))
(define-fun _281 () Real |main::irp_choice@3|)
(define-fun _282 () Bool (= _281 _7))
(define-fun _284 () Bool (and _280 _282))
(define-fun _287 () Real (- 1073741637))
(define-fun _288 () Real myStatus@5)
(define-fun _289 () Bool (= _288 _287))
(define-fun _290 () Bool (and _284 _289))
(define-fun _294 () Real s@6)
(define-fun _295 () Bool (= _203 _294))
(define-fun _297 () Real customIrp@6)
(define-fun _298 () Bool (= _297 _7))
(define-fun _300 () Real setEventCalled@6)
(define-fun _301 () Bool (= _297 _300))
(define-fun _303 () Real lowerDriverReturn@6)
(define-fun _304 () Bool (= _300 _303))
(define-fun _306 () Real compRegistered@6)
(define-fun _307 () Bool (= _303 _306))
(define-fun _309 () Real compFptr@6)
(define-fun _310 () Bool (= _306 _309))
(define-fun _312 () Real pended@6)
(define-fun _313 () Bool (= _309 _312))
(define-fun _318 () Real |__ADDRESS_OF_main::tmp_ndt_1|)
(define-fun _319 () Real (__BASE_ADDRESS_OF__ _318))
(define-fun _320 () Bool (= _318 _319))
(define-fun _322 () Real |main::tmp_ndt_1@3|)
(define-fun _323 () Bool (= _322 _206))
(define-fun _348 () Real (- 1))
(define-fun _360 () Real s@7)
(define-fun _379 () Bool (= _306 _7))
(define-fun _404 () Real 259)
(define-fun _418 () Bool (= _203 _360))
(define-fun _421 () Bool (not _418))
(define-fun _435 () Real lowerDriverReturn@7)
(define-fun _447 () Real |main::status@4|)
(define-fun _504 () Real |__ADDRESS_OF_IofCallDriver::Irp__PendingReturned|)
(define-fun _505 () Real (__BASE_ADDRESS_OF__ _504))
(define-fun _506 () Bool (= _504 _505))
(define-fun _508 () Real |__ADDRESS_OF_IofCallDriver::returnVal2|)
(define-fun _509 () Real (__BASE_ADDRESS_OF__ _508))
(define-fun _510 () Bool (= _508 _509))
(define-fun _512 () Real |__ADDRESS_OF_IofCallDriver::compRetStatus|)
(define-fun _513 () Real (__BASE_ADDRESS_OF__ _512))
(define-fun _514 () Bool (= _512 _513))
(define-fun _516 () Real |__ADDRESS_OF_IofCallDriver::__cil_tmp8|)
(define-fun _517 () Real (__BASE_ADDRESS_OF__ _516))
(define-fun _518 () Bool (= _516 _517))
(define-fun _522 () Real |IofCallDriver::Irp__PendingReturned@3|)
(define-fun _523 () Bool (= _522 _7))
(define-fun _528 () Real |IofCallDriver::returnVal2@3|)
(define-fun _531 () Real |__ADDRESS_OF_IofCallDriver::tmp_ndt_4|)
(define-fun _532 () Real (__BASE_ADDRESS_OF__ _531))
(define-fun _533 () Bool (= _531 _532))
(define-fun _535 () Real |IofCallDriver::tmp_ndt_4@3|)
(define-fun _536 () Bool (= _535 _7))
(define-fun _555 () Bool (= _528 _7))
(define-fun _573 () Bool (= _435 _528))
(define-fun _575 () Real |IofCallDriver::__retval__@2|)
(define-fun _576 () Bool (= _528 _575))
(define-fun _659 () Real compRegistered@7)
(define-fun _660 () Bool (= _659 _196))
(define-fun _662 () Real routine@4)
(define-fun _669 () Bool (= _659 _7))
(define-fun _672 () Bool (not _669))
(define-fun _674 () Bool (= _662 _7))
(define-fun _690 () Real (- 1073741802))
(define-fun _694 () Real |IofCallDriver::compRetStatus@3|)
(define-fun _697 () Real |IofCallDriver::__cil_tmp8@3|)
(define-fun _698 () Bool (= _694 _697))
(define-fun _700 () Bool (= _697 _690))
(define-fun _703 () Bool (not _700))
(define-fun _1260 () Real |__ADDRESS_OF_CdAudioDeviceControl::deviceExtension__Active|)
(define-fun _1261 () Real (__BASE_ADDRESS_OF__ _1260))
(define-fun _1262 () Bool (= _1260 _1261))
(define-fun _1264 () Real |__ADDRESS_OF_CdAudioDeviceControl::status|)
(define-fun _1265 () Real (__BASE_ADDRESS_OF__ _1264))
(define-fun _1266 () Bool (= _1264 _1265))
(define-fun _1268 () Real |CdAudioDeviceControl::deviceExtension__Active@3|)
(define-fun _1269 () Bool (= _1268 _206))
(define-fun _1272 () Bool (not _1269))
(define-fun _1274 () Bool (= _1268 _210))
(define-fun _1277 () Bool (not _1274))
(define-fun _1279 () Bool (= _1268 _196))
(define-fun _1282 () Bool (not _1279))
(define-fun _1284 () Bool (= _1268 _226))
(define-fun _1330 () Real |CdAudioDeviceControl::status@3|)
(define-fun _1333 () Real |__ADDRESS_OF_CdAudioHPCdrDeviceControl::currentIrpStack__Parameters__DeviceIoControl__IoControlCode|)
(define-fun _1334 () Real (__BASE_ADDRESS_OF__ _1333))
(define-fun _1335 () Bool (= _1333 _1334))
(define-fun _1337 () Real |__ADDRESS_OF_CdAudioHPCdrDeviceControl::tmp|)
(define-fun _1338 () Real (__BASE_ADDRESS_OF__ _1337))
(define-fun _1339 () Bool (= _1337 _1338))
(define-fun _1341 () Real |__ADDRESS_OF_CdAudioHPCdrDeviceControl::tmp___0|)
(define-fun _1342 () Real (__BASE_ADDRESS_OF__ _1341))
(define-fun _1343 () Bool (= _1341 _1342))
(define-fun _1345 () Real |__ADDRESS_OF_CdAudioHPCdrDeviceControl::__cil_tmp12|)
(define-fun _1346 () Real (__BASE_ADDRESS_OF__ _1345))
(define-fun _1347 () Bool (= _1345 _1346))
(define-fun _1349 () Real 147512)
(define-fun _1350 () Real |CdAudioHPCdrDeviceControl::__cil_tmp12@3|)
(define-fun _1351 () Bool (= _1350 _1349))
(define-fun _1353 () Real |CdAudioHPCdrDeviceControl::currentIrpStack__Parameters__DeviceIoControl__IoControlCode@3|)
(define-fun _1354 () Bool (= _1350 _1353))
(define-fun _1400 () Real |CdAudioHPCdrDeviceControl::__retval__@2|)
(define-fun _1417 () Real |__ADDRESS_OF_HPCdrCompletion::Irp__PendingReturned|)
(define-fun _1418 () Real (__BASE_ADDRESS_OF__ _1417))
(define-fun _1419 () Bool (= _1417 _1418))
(define-fun _1421 () Real |HPCdrCompletion::Irp__PendingReturned@3|)
(define-fun _1422 () Bool (= _1421 _7))
(define-fun _1425 () Bool (not _1422))
(define-fun _1427 () Bool (= _312 _7))
(define-fun _1432 () Real pended@7)
(define-fun _1433 () Bool (= _1432 _196))
(define-fun _1438 () Bool (<= _7 _288))
(define-fun _1441 () Bool (not _1438))
(define-fun _1466 () Real |HPCdrCompletion::__retval__@2|)
(define-fun _1467 () Bool (= _288 _1466))
(define-fun _1469 () Bool (= _694 _1466))
(define-fun _1518 () Real |CdAudioHPCdrDeviceControl::tmp@3|)
(define-fun _1519 () Bool (= _575 _1518))
(define-fun _1521 () Bool (= _1400 _1518))
(define-fun _1544 () Bool (= _1330 _1400))
(define-fun _4974 () Real |CdAudioDeviceControl::__retval__@2|)
(define-fun _4975 () Bool (= _1330 _4974))
(define-fun _4977 () Bool (= _447 _4974))
(define-fun _5042 () Real |main::we_should_unload@3|)
(define-fun _5043 () Bool (= _5042 _7))
(define-fun _5162 () Bool (= _447 _348))
(define-fun _5163 () Bool (not _5162))
(define-fun _5187 () Bool (= _447 _404))
(define-fun _5188 () Bool (not _5187))
(define-fun _7099 () Bool (and _290 _295))
(define-fun _7100 () Bool (and _298 _7099))
(define-fun _7101 () Bool (and _301 _7100))
(define-fun _7102 () Bool (and _304 _7101))
(define-fun _7103 () Bool (and _307 _7102))
(define-fun _7104 () Bool (and _310 _7103))
(define-fun _7105 () Bool (and _313 _7104))
(define-fun _7106 () Bool (and _252 _7105))
(define-fun _7107 () Bool (and _320 _7106))
(define-fun _7108 () Bool (and _323 _7107))
(define-fun _7109 () Bool (and _1262 _7108))
(define-fun _7110 () Bool (and _1266 _7109))
(define-fun _7111 () Bool (and _1272 _7110))
(define-fun _7112 () Bool (and _1277 _7111))
(define-fun _7113 () Bool (and _1282 _7112))
(define-fun _7114 () Bool (and _1284 _7113))
(define-fun _7115 () Bool (and _1335 _7114))
(define-fun _7116 () Bool (and _1339 _7115))
(define-fun _7117 () Bool (and _1343 _7116))
(define-fun _7118 () Bool (and _1347 _7117))
(define-fun _7119 () Bool (and _1351 _7118))
(define-fun _7120 () Bool (and _1354 _7119))
(define-fun _7121 () Bool (and _295 _7120))
(define-fun _7122 () Bool (and _379 _7121))
(define-fun _7123 () Bool (and _660 _7122))
(define-fun _7124 () Bool (and _674 _7123))
(define-fun _7125 () Bool (and _506 _7124))
(define-fun _7126 () Bool (and _510 _7125))
(define-fun _7127 () Bool (and _514 _7126))
(define-fun _7128 () Bool (and _518 _7127))
(define-fun _7129 () Bool (and _672 _7128))
(define-fun _7130 () Bool (and _674 _7129))
(define-fun _7131 () Bool (and _1419 _7130))
(define-fun _7132 () Bool (and _1425 _7131))
(define-fun _7133 () Bool (and _1427 _7132))
(define-fun _7134 () Bool (and _1433 _7133))
(define-fun _7135 () Bool (and _1441 _7134))
(define-fun _7136 () Bool (and _1467 _7135))
(define-fun _7137 () Bool (and _1469 _7136))
(define-fun _7138 () Bool (and _698 _7137))
(define-fun _7139 () Bool (and _703 _7138))
(define-fun _7140 () Bool (and _523 _7139))
(define-fun _7141 () Bool (and _533 _7140))
(define-fun _7142 () Bool (and _536 _7141))
(define-fun _7143 () Bool (and _555 _7142))
(define-fun _7144 () Bool (and _295 _7143))
(define-fun _7145 () Bool (= _227 _360))
(define-fun _7146 () Bool (and _7144 _7145))
(define-fun _7147 () Bool (and _573 _7146))
(define-fun _7148 () Bool (and _576 _7147))
(define-fun _7149 () Bool (and _1519 _7148))
(define-fun _7150 () Bool (and _1521 _7149))
(define-fun _7151 () Bool (and _1544 _7150))
(define-fun _7152 () Bool (and _4975 _7151))
(define-fun _7153 () Bool (and _4977 _7152))
(define-fun _7154 () Bool (and _5043 _7153))
(define-fun _7155 () Bool (and _1433 _7154))
(define-fun _7156 () Bool (and _421 _7155))
(define-fun _7157 () Bool (and _1433 _7156))
(define-fun _7158 () Bool (= _223 _360))
(define-fun _7160 () Bool (not _7158))
(define-fun _7161 () Bool (and _7157 _7160))
(define-fun _7162 () Bool (= _200 _360))
(define-fun _7163 () Bool (not _7162))
(define-fun _7165 () Bool (and _7161 _7163))
(define-fun _7166 () Bool (and _5163 _7165))
(define-fun _7167 () Bool (= _215 _360))
(define-fun _7168 () Bool (not _7167))
(define-fun _7170 () Bool (and _7166 _7168))
(define-fun _7173 () Bool (and _7145 _7170))
(define-fun _7174 () Bool (and _1433 _7173))
(define-fun _7175 () Bool (and _5188 _7174))



(assert _7175)
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
